Nuprl Lemma : l_all-nil
0,22
postcript
pdf
T
:Type,
P
:Top. (
x
nil.
P
(
x
))
True
latex
Definitions
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
P
Q
,
False
,
A
,
A
B
,
i
j
,
,
t
...$L
,
x
(
s
)
,
Prop
,
A
&
B
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
x
L
.
P
(
x
)
,
True
,
x
.
t
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
l
all
wf
,
true
wf
,
l
member
wf
,
length
nil
,
length
wf2
,
top
wf
origin
T:Type, P:Top. (x
nil. P(x)) 
True T:Type, P:Top. (xnil. P(x)) True Tx:A. B(x)
Q
A
B
j
x:A. B(x) l)xL. P(x)
x. t(x) Q Q